\begin{tabbing}
$\forall$${\it es}$:ES, $A$:Type, $X$:AbsInterface($A$).
\\[0ex]$X$ is finite
\\[0ex]$\Rightarrow$ ($\exists$\=${\it locs}$:Id List\+
\\[0ex]$\exists$\=${\it knds}$:Id$\rightarrow$(Knd List)\+
\\[0ex]($\forall$$e$:E. ($\uparrow$($e$ $\in_{b}$ $X$)) $\Rightarrow$ ((loc($e$) $\in$ ${\it locs}$) \& (kind($e$) $\in$ ${\it knds}$(loc($e$))))))
\-\-
\end{tabbing}